package ch.epfl.lara.matcheck.verify.spec;

import ch.epfl.lara.matcheck.ast._
import ch.epfl.lara.matcheck.verify.provers.ProverResults
import ch.epfl.lara.matcheck.verify.transform.TreeExpr2Formula

class ProgramSpecVerifier extends SpecVerifier {

  
  private var objects: List[ObjectDef] = _
  private var classes: List[ClassDef] = _
  
  def this(program: Program) = {
    this()
    this.objects = program.objects
    this.classes = program.classes
    verifyProgram()
  }
  
  private def verifyProgram() {
    verifyMethods()
  }
  
  private def verifyMethods() {
    Timer.startPostconditionVerification()
    
    for(obj<-objects;method<-obj.methods)  {
      Report.verbose("> Analysing method "+method.getName+" in object "+obj.getName)
      MethodSpecVerifier(method)
    }
    for(klass<-classes;method<-klass.methods) {
      Report.verbose("> Analysing method "+method.getName+" in class "+klass.getName)
      MethodSpecVerifier(method)
    }
    
    Timer.finishedPostconditionVerification()
  }
  

  override protected def startTimer() {

  }
  
  override protected def stopTimer() {

  }
  
  
}

